i, x:Id, k:Knd, ds:a:Id fp Type, da:a:Knd fp Type, f:(State(ds)Valtype(da;k)ds(x)?Void).
@i: with declarations ds:dsda:daeffect of k(v) is x := f s v  Dsys
& (D:Dsys.
& (@i: with declarations ds:dsda:daeffect of k(v) is x := f s v  D
& ( D 
& ( realizes es.
& ( (x:Id. vartype(i;x)  ds(x)?Top)
& ( & (e:E. loc(e) = i  Id  valtype(e)  Valtype(da;kind(e)))
& ( & ((isrcv(k)  destination(lnk(k)) = i)  kindtype(i;k)  Valtype(da;k))
& ( & (e:E.
& ( & (loc(e) = i  Id
& ( & ( kind(e) = k  Knd
& ( & ( (x after e) = f((state when e),val(e))  ds(x)?Top)) 

latex

Definitions

Id, t  T, x:A. B(x), P  Q, x:AB(x), Atom$n, left+right, Knd, x:AB(x), a:A fp B(a), s = t, Dsys, {x:A| B(x) }, 1of(t), E, Top, IdDeq, Type, x.A(x), x. t(x), f(x)?z, vartype(i;x), state@i, Valtype(da;k), valtype(e), val(e), {T}, SQType(T), Prop, s ~ t, (state when e), State(ds), Void, f(a), (x after e), P & Q, kind(e), loc(e), kindtype(i;k), lnk(k), destination(l), isrcv(k), b, A & B, es is an event system of D, ES, D1  D2, D realizes es. P(es), , MsgA, a = b, if b t else f fi, @i: A, @i: with declarations ds:dsda:daeffect of k(v) is x := f s v, with declarations ds:dsda:daeffect of k(v) is x := f s v

Lemmas

effect-rule, ma-state wf, fpf wf, ifthenelse wf, eq id wf, msga wf, ma-single-effect wf, ma-empty wf, dsys wf, realizes-monotone-wrt-sub, event system wf, d-es wf, assert wf, isrcv wf, ldst wf, lnk wf, es-kindtype wf, es-E wf, es-loc wf, Knd wf, es-kind wf, es-after wf, fpf-cap-void-subtype, es-state-when wf, Id sq, es-val wf, es-state wf, es-valtype wf, ma-valtype wf, subtype rel dep function, es-vartype wf, fpf-cap wf, id-deq wf, top wf, Id wf